/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2003  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: JBddManager.java,v 1.19 2004/06/03 03:54:01 fqian Exp $

package SableJBDD.bdd;

import SableJBDD.bdd.internal.*;
import SableJBDD.cache.*;

import java.util.Set;
import java.util.HashSet;
import java.util.Map;
import java.util.Iterator;
import java.io.*;

/** 
 * A BDD manager manages system resources such as unique table and caches.
 *
 * @author Feng Qian
 */
public class JBddManager implements JBddConstants{

  private static final boolean DEBUG = true;

  // a list of bdd variables
  private JBddVariable[] bddVariables;  // a list of bdd variables
  // the index of variable at each level, excluding constants.
  // 0 is the top level.
  private int[] varOrdering;
  
  private int numberOfVariables;        // the number of valid bdd vars

  // indexed by level
  private JBDD[] cachedPosBDDs;         // cached positive bdds of a variable
  private JBDD[] cachedNegBDDs;         // cached negative bdds of a variable

  // internal tables and caches
  protected UniqueTable       uniqueTable;   // the unique table
  protected BddCache          iteCache;      // the ite cache
  protected BddCache          applyCache;    // the apply cache
  protected BddCache          quantCache;    // the quantification cache

  // this has to be a good prime number, fix it later
  private static int DEFAULT_UNIQUE_TABLE_ENTRIES = (1 << 10);
  private static int DEFAULT_CACHE_SIZE           = (1 << 10);
  private static int DEFAULT_CACHE_ASSOCIATIVITY  = 2;

  // some prime numbers, see http://www.utm.edu/research/primes/lists/2small/0bit.html
  // 
  // small ones, 2^10 - 3, 2^10 - 5, 2^10 - 15
  //             2^12 - 3, 2^12 - 5, 2^12 - 17
  //             2^14 - 3, 2^14 - 15, 2^13 - 21
  //             2^16 - 15, 2^16 - 17, 2^16 - 39
  //             2^18 - 5, 2^18 - 11, 2^18 - 17
  // medium ones, 2^20 - 3, 2^20 - 5, 2^20 - 17
  // large ones, 2^30 - 35, 2^30 - 41, 2^30 - 83
  
    
  /**
   * Defines a JBDD manager without variables. Variables will be created later
   * when necessary.
   */
  public JBddManager() {
    this(0);
  }

  /**
   * Defines a JBDD manager with a specified number of variables.
   * @param initNumberOfVariables
   */
  public JBddManager(int initNumberOfVariables) {
    int initOrdering[] = new int[initNumberOfVariables];
    for (int i=0; i<initNumberOfVariables; i++) {
      initOrdering[i] = i;
    }
    initializeManager(initOrdering);
  }

  /**
   * Defines a JBDD manager with a specific variable ordering.
   * @param initVariableOrdering the number of variables and
   *        the order of each variable. The value at index i is the ith
   *        variable's order.
   */
  public JBddManager(int[] initVariableOrdering) {
    initializeManager(initVariableOrdering);
  }
 
  ///////////////////////////////////////////
  // Configurations
  ///////////////////////////////////////////
  
  // unique table properties
  private int UniqueTableSize;
  private int UniqueTableKind;
    // pooling strategy and initial pool size when using weak unique table
    private int PoolingStrategy;
    private int NodePoolSize;
  
  // cache properties
  private int CacheKind;
  private int CacheSize;
  private int CacheAssociativities;

  private int getIntProperty(String propname, int defaultsize) {
    String prop = System.getProperty(propname, Integer.toString(defaultsize));
    try {
      return Integer.parseInt(prop);
    } catch (NumberFormatException e) {
      System.err.println(propname+" must be an integer : "+prop);
      System.exit(-1);
    }
    return -1;
  }

  private void getDefaultSettings() {
    // get parameters passed in by VM command line options
    // uniquetable.size
    this.UniqueTableSize = Prime.getSmallestPrimeGTE(getIntProperty("uniquetable.size", 
                                                                    DEFAULT_UNIQUE_TABLE_ENTRIES));
    
    // uniquetable.kind : regular, soft, weak
    String uniqueTableKindProp = System.getProperty("uniquetable.kind", "weak");
    if (uniqueTableKindProp.equals("regular")) {
      this.UniqueTableKind = REGULAR_REF;
    } else if (uniqueTableKindProp.equals("soft")) {
      this.UniqueTableKind = SOFT_REF;
    } else if (uniqueTableKindProp.equals("weak")) {
      this.UniqueTableKind = WEAK_REF;
    } else if (uniqueTableKindProp.equals("phantom")) {
      this.UniqueTableKind = PHANTOM_REF;
    } else {
      System.err.println("unsupported option : uniquetable.kind = "+uniqueTableKindProp);
      System.exit(-1);
    }
    
    if (this.UniqueTableKind == WEAK_REF) {
      // pooling.strategy : none, prealloc, fixed, expandible, dynamic 
      String poolingStrategyProp = System.getProperty("pooling.strategy", "dynamic");
      if (poolingStrategyProp.equals("none")) {
        // no preallocation
        this.PoolingStrategy = NO_POOLING; 
      } else if (poolingStrategyProp.equals("prealloc")) {
        // preallocation only, no recycling
        this.PoolingStrategy = PRE_ALLOCATION;
        this.NodePoolSize = getIntProperty("pooling.size", DEFAULT_PRE_ALLOC_SIZE);    
      } else if (poolingStrategyProp.equals("fixed")) {
        // only recycle pre-allocated nodes
        this.PoolingStrategy = FIXED_SIZE;
        this.NodePoolSize = getIntProperty("pooling.size", DEFAULT_FIXED_POOL_SIZE);
      } else if (poolingStrategyProp.equals("expandible")) {
        // recycles all allocated nodes
        this.PoolingStrategy = EXPANDIBLE;
        this.NodePoolSize = getIntProperty("pooling.size", DEFAULT_EXPANDIBLE_SIZE);
      } else if (poolingStrategyProp.equals("dynamic")) {
        // recycles most recently allocated nodes
        this.PoolingStrategy = DYNAMIC;
        this.NodePoolSize = getIntProperty("pooling.size", DEFAULT_DYNA_POOL_SIZE);
      } else {
        System.err.println("unsupported option : pooling.strategy = "+poolingStrategyProp);
        System.exit(-1);
      }
    } else if (this.UniqueTableKind == PHANTOM_REF) {
      this.NodePoolSize = getIntProperty("pooling.size", DEFAULT_PHANTOM_POOL_SIZE);
    }
    
    // cache.kind : regular, soft
    String cacheKindProp = System.getProperty("cache.kind", "none");
    if (cacheKindProp.equals("none")) {
      // donot use cache
      this.CacheKind = NO_CACHE;
    } else if (cacheKindProp.equals("regular")) {
      // use regular cache
      this.CacheKind = REGULAR_REF;
    } else if (cacheKindProp.equals("soft")) {
      this.CacheKind = SOFT_REF;
    } else {
      System.err.println("unsupported options : cache.kind = "+cacheKindProp);
      System.exit(-1);
    }

    // cache.size
    this.CacheSize = Prime.getSmallestPrimeGTE(getIntProperty("cache.size", DEFAULT_CACHE_SIZE));
    
    // cache.associativity 0(ideal), 1, more
    this.CacheAssociativities = getIntProperty("cache.associativities", 
                                               DEFAULT_CACHE_ASSOCIATIVITY);
  }
  // initialize the manager with a specific ordering
  private void initializeManager(int[] initVariableOrdering) {
    getDefaultSettings();
    createTablesAndCaches();

    int initNumberOfVariables = initVariableOrdering.length;
    
    this.bddVariables = new JBddVariable[initNumberOfVariables];
    this.varOrdering  = new int[initNumberOfVariables];
    
    this.numberOfVariables = initNumberOfVariables;
    
    this.cachedPosBDDs = new JBDD[initNumberOfVariables];
    this.cachedNegBDDs = new JBDD[initNumberOfVariables];

    // make default variables
    for (int i=0; i<initNumberOfVariables; i++) {
      int level = initVariableOrdering[i];
      this.bddVariables[i] = new JBddVariable("v"+i, level);
      this.varOrdering[level]  = i;
    }

    JBddManager.BDDOPERATORS = new UniqueInteger[TOTAL_BDDOPS];
    for (int i=0; i<TOTAL_BDDOPS; i++) {
      JBddManager.BDDOPERATORS[i] = new UniqueInteger(i);
    }
  }

  private void createTablesAndCaches() {
    //if (DEBUG) printConfigurations(System.out);

    switch (this.UniqueTableKind) {
    case REGULAR_REF:
      this.uniqueTable = new RegularUniqueTable(this.UniqueTableSize);
      break;
    case SOFT_REF:
      this.uniqueTable = new SoftUniqueTable(this.UniqueTableSize);
      break;
    case WEAK_REF:
      // add pool types
      switch (this.PoolingStrategy) {
      case NO_POOLING:
        this.uniqueTable = new WeakUniqueTable(this.UniqueTableSize,
                                             new DummyNodePool());
        break;
      case PRE_ALLOCATION:
        this.uniqueTable = new WeakUniqueTable(this.UniqueTableSize,
                                 new NonReclaimableNodePool(this.NodePoolSize));
        break;
      case FIXED_SIZE:
        this.uniqueTable = new WeakUniqueTable(this.UniqueTableSize,
                                 new FixedSizeNodePool(this.NodePoolSize));
        break;
      case EXPANDIBLE:
        this.uniqueTable = new WeakUniqueTable(this.UniqueTableSize,
                                 new ExpandibleNodePool(this.NodePoolSize));
        break;
      case DYNAMIC:
        this.uniqueTable = new WeakUniqueTable(this.UniqueTableSize,
                                 new DynamicNodePool(this.NodePoolSize));
        break;
      default:
        assert false: "invalid pooling strategy "+this.PoolingStrategy;
        break;
      }
      break;
    case PHANTOM_REF:
      this.uniqueTable = new PhantomUniqueTable(this.UniqueTableSize, this.NodePoolSize);
      break;
    default:
      assert false : "invalid unique table kind "+UniqueTableKind;
      break;
    }

    TripleIntKeyCache iteImpl = null, applyImpl = null, quantImpl = null;
    if (this.CacheAssociativities == IDEAL) {
      iteImpl = applyImpl = quantImpl = new IdealCache(this.CacheSize);
    } else if (this.CacheAssociativities == ONEWAY) {
      iteImpl = new OneWayCache(this.CacheSize);
      applyImpl = new OneWayCache(this.CacheSize);
      quantImpl = new OneWayCache(this.CacheSize);
    } else {
      iteImpl = new MultiWayCache(this.CacheSize, 
                                  this.CacheAssociativities);
      applyImpl = new MultiWayCache(this.CacheSize, 
                                    this.CacheAssociativities);
      quantImpl = new MultiWayCache(this.CacheSize, 
                                    this.CacheAssociativities);
    }

    switch (this.CacheKind) {
    case NO_CACHE:
      this.iteCache   = new EmptyBddCache();
      this.applyCache = new EmptyBddCache();
      this.quantCache = new EmptyBddCache();
      break;
    case REGULAR_REF:
      this.iteCache   = new RegularBddCache(iteImpl);
      this.applyCache = new RegularBddCache(applyImpl);
      this.quantCache = new RegularBddCache(quantImpl);
      break;
    case SOFT_REF:
      this.iteCache   = new SoftBddCache(iteImpl);
      this.applyCache = new SoftBddCache(applyImpl);
      this.quantCache = new SoftBddCache(quantImpl);
      break;
    default:
      assert false : "invalid cache table kind "+this.CacheKind;
      break;
    }
  }

  ///////////////////////////////////////////////////////////
  //  Implementations
  ///////////////////////////////////////////////////////////
  /**
   * @return the number of variables.
   */
  public int getNumberOfVariables() {
    return this.numberOfVariables;
  }

  /**
   * @return ith variable.
   */
  public JBddVariable getIthVariable(int i) {
    return this.bddVariables[i];
  }
  
  /**
   * @return the index of variable at a specific order.
   */
  public int getVariableIndexAtLevel(int l) {
    return this.varOrdering[l];
  }
  
  /**
   * @return a variable at a specific order.
   */
  public JBddVariable getVariableAtLevel(int l) {
    return this.bddVariables[this.varOrdering[l]];
  }
  
  /**
   * Creates a new bdd variable with a name, it is automatically allocated at 
   * the top level.
   * @param name the variable name
   * @return the newly created bdd variable
   */
  public synchronized JBddVariable newVariable(String name) {
    checkAndExpandVariableArray(this.numberOfVariables);
    JBddVariable newvar = new JBddVariable(name, this.numberOfVariables);
    this.bddVariables[this.numberOfVariables] = newvar;
    this.varOrdering[this.numberOfVariables] = this.numberOfVariables;
    this.numberOfVariables++;
    
    boolean bingo = verifyIntegrityOfVariablesAndOrdering();
    assert bingo;

    return newvar;
  }

  // check if a variable is in the range, expand the array of variables 
  // if necessary.
  private void checkAndExpandVariableArray(int newindex) {
    if (newindex >= this.bddVariables.length) {
      int newlength = newindex + 4;
      int oldlength = this.bddVariables.length;
      
      // expand the variable array
      JBddVariable[] newvars = new JBddVariable[newlength];
      System.arraycopy(this.bddVariables, 0, newvars, 0, 
                       oldlength);
      this.bddVariables = newvars;

      // expand the order array
      int[] neworder = new int[newlength];
      System.arraycopy(this.varOrdering, 0, neworder, 0,
                       oldlength);
      this.varOrdering = neworder;
      
      // expand cached JBDDs
      JBDD[] newPosBDDs = new JBDD[newlength];
      System.arraycopy(this.cachedPosBDDs, 0, newPosBDDs, 0, 
                       oldlength);
      this.cachedPosBDDs = newPosBDDs;

      JBDD[] newNegBDDs = new JBDD[newlength];
      System.arraycopy(this.cachedNegBDDs, 0, newNegBDDs, 0,
                       oldlength);
      this.cachedNegBDDs = newNegBDDs;
    }
  }

  /**
   * Gets or creates a new bdd variable at a specific order (level).
   * If the level is above the top level of current bdd varaibles,
   * all variables under the specific level will be created.
   * @param level the level at which a new bdd variable is created
   * @return the newly created variable
   */
  public synchronized JBddVariable newVariableAtLevel(int level) {
    assert (level >= 0);
      
    if (level < this.numberOfVariables) return this.bddVariables[level];

    checkAndExpandVariableArray(level+1+4);
    
    for (int i=this.numberOfVariables; i<=level; i++) {
      this.bddVariables[i] = new JBddVariable("v"+i, i);
      this.varOrdering[i] = i;
    } 
    this.numberOfVariables = level+1;
  
    boolean bingo = verifyIntegrityOfVariablesAndOrdering();
    assert bingo;

    return this.bddVariables[level];
  }
 
  // check the consistancy between ordering and variables.
  private boolean verifyIntegrityOfVariablesAndOrdering() {
    for (int i=0; i<this.numberOfVariables; i++) {
      if (this.varOrdering[this.bddVariables[i].getLevel()] != i)
        return false;
    }
    return true;
  }
 
  /**
   * @return the constant ONE function
   */
  public JBDD ONE() {
    return new JBDD(this, JBddConstNode.ONE());
  }

  /**
   * @return the constant ZERO function
   */
  public JBDD ZERO() {
    return new JBDD(this, JBddConstNode.ZERO());
  }

  /**
   * Gets a BDD function representing the positive form of a variable.
   * posBddOf and negBddOf are called very frequently,
   * they donot require synchronized since if two threads writes
   * to the same cache, two cached variables are both valid.
   *
   * @param var the bdd variable
   * @return the BDD function
   */
  public JBDD posBddOf(JBddVariable var) {
    // look up cached bdds first
    JBDD bdd = lookupCachedBDDs(var, this.cachedPosBDDs);
    if (bdd == null) {
      bdd = new JBDD(this,
                     makenode_internal(var, JBddConstNode.ZERO(), JBddConstNode.ONE())
                     );
      this.cachedPosBDDs[var.getLevel()] = bdd;
    }
    return bdd.copy();
  }

  /**
   * Gets a BDD function representing the negative form of a variable
   * 
   * @param var the bdd variable
   * @return the BDD function
   */
  public JBDD negBddOf(JBddVariable var) {
    // look up cached 
    JBDD bdd = lookupCachedBDDs(var, this.cachedNegBDDs);
    if (bdd == null) {
      bdd = new JBDD(this,
                     makenode_internal(var, JBddConstNode.ONE(), JBddConstNode.ZERO())
                     );
      this.cachedNegBDDs[var.getLevel()] = bdd;
    }
    return bdd.copy();
  }
  
  private JBDD lookupCachedBDDs(JBddVariable var, JBDD[] cache) {
    // since varaible can reordered, the cache maybe invalidated at that time
    int level = var.getLevel();
    if (cache[level] == null) return null;
    if (!cache[level].isRootOf(var)) {
      return null;
    } else {
      return cache[level];
    }
  }

  // make a bdd node by given variable, low and high bdds
  // this routine first consults unique table
  private JBddNode makenode_internal(JBddVariable var,
                                     JBddNode low,
                                     JBddNode high) {
    if (low == high) return low;  // quickly simplify
    
    assert (var.getLevel() < low.getLevel() && var.getLevel() < high.getLevel()): var;
    
    return this.uniqueTable.findOrCreate(var, low, high);
  }

  ////////////////////////////////////////////////////////
  // internal impl. of basic bdd operations
  ////////////////////////////////////////////////////////

  // bdd op used by apply
  protected final static int BDDOP_AND     =  0;
  protected final static int BDDOP_OR      =  1;
  protected final static int BDDOP_NAND    =  2;
  protected final static int BDDOP_NOR     =  3;
  protected final static int BDDOP_XOR     =  4;
  protected final static int BDDOP_IMPLY   =  5;
  protected final static int BDDOP_BI_IMPLY  = 6;
  protected final static int BDDOP_DIFF    = 7;
  protected final static int BDDOP_LESS    =  8;

  // bdd op cannot used by apply
  protected final static int BDDOP_NOT     =  9;
  protected final static int BDDOP_SIMPLIFY = 10;

  protected final static int TOTAL_BDDOPS   = 11;
  protected static UniqueInteger[] BDDOPERATORS; 
  
  // x & y
  protected JBddNode AND(JBddNode x, JBddNode y) {
    if (x == y) return x;
        
        // handling base cases
    if (x == JBddConstNode.ZERO() || y == JBddConstNode.ZERO()) 
      return JBddConstNode.ZERO();
    if (x == JBddConstNode.ONE()) return y;
    if (y == JBddConstNode.ONE()) return x;

    // make standard 
    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_AND);
    } else {
      return apply_internal(y, x, BDDOP_AND);
    }
  }

  // x | y
  protected JBddNode OR(JBddNode x, JBddNode y) {
    assert x != null && y != null;

    if (x == y) return x;
        
        // handling base cases
    if (x == JBddConstNode.ONE() || y == JBddConstNode.ONE()) 
      return JBddConstNode.ONE();
    if (x == JBddConstNode.ZERO()) return y;
    if (y == JBddConstNode.ZERO()) return x;
    
    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_OR);
    } else {
      return apply_internal(y, x, BDDOP_OR);
    }
  }

  // ! (x & y)
  protected JBddNode NAND(JBddNode x, JBddNode y) {
    // handling base cases
    if (x == JBddConstNode.ZERO() || y == JBddConstNode.ZERO())
      return JBddConstNode.ONE();
    if (x == JBddConstNode.ONE()) return NOT(y);
    if (y == JBddConstNode.ONE()) return NOT(x);

    if (x == y) return NOT(x);

    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_NAND);
    } else {
      return apply_internal(y, x, BDDOP_NAND);
    }
  }

  // ! (x | y)
  protected JBddNode NOR(JBddNode x, JBddNode y) {
    // handle base cases
    if (x == JBddConstNode.ONE() || y == JBddConstNode.ONE())
      return JBddConstNode.ZERO();
    if (x == JBddConstNode.ZERO()) return NOT(y);
    if (x == JBddConstNode.ZERO()) return NOT(x);

    if (x == y) return NOT(x);

    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_NOR);
    } else {
      return apply_internal(y, x, BDDOP_NOR);
    }
  }

  // x ^ y
  protected JBddNode XOR(JBddNode x, JBddNode y) {
    if (x == y) return JBddConstNode.ZERO();
    if (x == JBddConstNode.ONE() && y == JBddConstNode.ZERO())
      return JBddConstNode.ONE();
    if (x == JBddConstNode.ZERO() && y == JBddConstNode.ONE())
      return JBddConstNode.ONE();

    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_XOR);
    } else {
      return apply_internal(y, x, BDDOP_XOR);
    }
  }

  // x -> y ( !x | y )
  protected JBddNode IMPLY(JBddNode x, JBddNode y) {
    if (x == JBddConstNode.ZERO()) return JBddConstNode.ONE();
    if (x == JBddConstNode.ONE()) return y;
    if (y == JBddConstNode.ONE()) return JBddConstNode.ONE();

    return apply_internal(x, y, BDDOP_IMPLY);
  }
 
  // x <-> y
  protected JBddNode BI_IMPLY(JBddNode x, JBddNode y) {
    if (x.isConst() && y.isConst()) { // two virtual calls
      if (x == y) 
        return JBddConstNode.ONE();
      else 
        return JBddConstNode.ZERO();
    }
  
    // alternate implementation
    /*
    if ( (x == JBddConstNode.ZERO() && y == JBddConstNode.ZERO())
      || (x == JBddConstNode.ONE()  && y == JBddConstNode.ONE()))
      return JBddNode.ONE();
    if ( (x == JBddConstNode.ONE()  && y == JBddConstNode.ZERO())
      || (x == JBddConstNode.ZERO() && y == JBddConstNode.ONE()))
      return JBddNode.ZERO();
    */
    if (x.getLevel() > y.getLevel()) {
      return apply_internal(x, y, BDDOP_BI_IMPLY);
    } else {
      return apply_internal(y, x, BDDOP_BI_IMPLY);
    }
  }

  // greater than
  protected JBddNode DIFF(JBddNode x, JBddNode y) {
    if (x.isConst() && y.isConst()) {
      if (x == JBddConstNode.ONE() && y == JBddConstNode.ZERO())
        return JBddConstNode.ONE();
      else
        return JBddConstNode.ZERO();
    }

    // alternate implementation
    /*
    if (x == JBddConstNode.ONE() && y == JBddConstNode.ZERO())
      return JBddConstNode.ONE();
    if ( (x == JBddConstNode.ONE()  && y == JBddConstNode.ONE() )
      || (x == JBddConstNode.ZERO() && y == JBddConstNode.ONE() )
      || (x == JBddConstNode.ZERO() && y == JBddConstNode.ZERO())
      return JBddConstNode.ZERO();
    */
    
    return apply_internal(x, y, BDDOP_DIFF);
  }

  // less than
  protected JBddNode LESS(JBddNode x, JBddNode y) {
    if (x.isConst() && y.isConst()) {
      if (x == JBddConstNode.ZERO() && y == JBddConstNode.ONE())
        return JBddConstNode.ONE();
      else
        return JBddConstNode.ZERO();
    }

    // alternate impl.
    /*
    if (x == JBddConstNode.ZERO() && y == JBddConstNode.ONE())
      return JBddConstNode.ONE();
    if ( (x == JBddConstNode.ONE()  && y == JBddConstNode.ONE() )
      || (x == JBddConstNode.ONE()  && y == JBddConstNode.ZERO() )
      || (x == JBddConstNode.ZERO() && y == JBddConstNode.ZERO())
      return JBddConstNode.ZERO();
    */

    return apply_internal(x, y, BDDOP_LESS);
  }
    
  // ! x
  protected JBddNode NOT(JBddNode x) {
    if (x == JBddConstNode.ONE()) return JBddConstNode.ZERO();
    if (x == JBddConstNode.ZERO()) return JBddConstNode.ONE();

    // check cache
    JBddNode result = applyCache.lookup(x, x, JBddManager.BDDOPERATORS[BDDOP_NOT]);
    if (result != null) return result;
    
    result = makenode_internal(x.variable, NOT(x.low), NOT(x.high));
    
    // cache results
    applyCache.put(x, x, JBddManager.BDDOPERATORS[BDDOP_NOT], result);
    return result;
  }

  ////////////////////////////////////////////////////////
  // IMPLEMENTATION
  //
  // NOTE: operations in this class assume each BDD node is unique;
  //       therefore, comparison is made by comparing pointers instead
  //       of calling 'equals' method.
  ////////////////////////////////////////////////////////
  // apply function of bdd node
  //
  private JBddNode apply_internal(JBddNode x, JBddNode y, int op) {
    // check the apply cache
    JBddNode result = applyCache.lookup(x, y, JBddManager.BDDOPERATORS[op]);
    if (result != null) return result;

    JBddVariable var;
    JBddNode xlow, ylow, xhigh, yhigh;
    
    // perform computation here
    if (x.getLevel() == y.getLevel()) {
      if (x.isConst()) {
        assert y.isConst();

        // base case
        xlow = x; xhigh = x;
        ylow = y; yhigh = y;
        var = x.variable;
      } else {
        xlow = x.low; ylow = y.low;
        xhigh = x.high; yhigh = y.high;
        var = x.variable;
      }
    } else if (x.getLevel() < y.getLevel()) {
      xlow = x.low; ylow = y;
      xhigh = x.high; yhigh = y;
      var = x.variable;
    } else {
      xlow = x; ylow = y.low;
      xhigh = x; yhigh = y.high;
      var = y.variable;
    }
    
    JBddNode rlow, rhigh;
    switch (op) {
    case BDDOP_AND:
      rlow = AND(xlow, ylow);
      rhigh = AND(xhigh, yhigh);
      break;
    case BDDOP_OR:
      rlow = OR(xlow, ylow);
      rhigh = OR(xhigh, yhigh);
      break;
    case BDDOP_NAND:
      rlow = NAND(xlow, ylow);
      rhigh = NAND(xhigh, yhigh);
      break;
    case BDDOP_NOR:
      rlow = NOR(xlow, ylow);
      rhigh = NOR(xhigh, yhigh);
      break;
    case BDDOP_XOR:
      rlow = XOR(xlow, ylow);
      rhigh = XOR(xhigh, yhigh);
      break;
    case BDDOP_IMPLY:
      rlow = IMPLY(xlow, ylow);
      rhigh = IMPLY(xhigh, yhigh);
      break;
    case BDDOP_BI_IMPLY:
      rlow = BI_IMPLY(xlow, ylow);
      rhigh = BI_IMPLY(xhigh, yhigh);
      break;
    case BDDOP_DIFF:
      rlow = DIFF(xlow, ylow);
      rhigh = DIFF(xhigh, yhigh);
      break;
    case BDDOP_LESS:
      rlow = LESS(xlow, ylow);
      rhigh = LESS(xhigh, yhigh);
      break;
    default:
      throw new RuntimeException("BDDOP "+op+" is not supported by apply");
    }

    result = makenode_internal(var, rlow, rhigh);

    // cache the result
    applyCache.put(x, y, JBddManager.BDDOPERATORS[op], result);

    return result;
  }


  ////////////////////////////////////////////////////
  // More advanced operations
  ////////////////////////////////////////////////////
  // if (x) then y else z
  protected JBddNode ITE(JBddNode x, JBddNode y, JBddNode z) {
    assert (x != null && y != null && z != null);
    
    if (x == JBddConstNode.ONE()) return y;
    if (x == JBddConstNode.ZERO()) return z;
    if (y == z) return y;
    if (y == JBddConstNode.ONE() && z == JBddConstNode.ZERO())
      return x;
    if (y == JBddConstNode.ZERO() && z == JBddConstNode.ONE())
      return NOT(x);

    // look up caches
    JBddNode result = this.iteCache.lookup(x, y, z);
    if (result != null) return result;

    // find the least level among x, y, z
    int minlevel = MAX_LEVEL;
    JBddVariable minvar = null;
    if (minlevel > x.getLevel()) {
      minlevel = x.getLevel();
      minvar   = x.variable;
    }
    if (minlevel > y.getLevel()) {
      minlevel = y.getLevel();
      minvar   = y.variable;
    }
    if (minlevel > z.getLevel()) {
      minlevel = z.getLevel();
      minvar   = z.variable;
    }

    assert (minlevel != MAX_LEVEL && minvar != null) : minlevel;

    JBddNode xlow, ylow, zlow, xhigh, yhigh, zhigh;
    if (x.getLevel() == minlevel) {
      xlow = x.low; xhigh = x.high;
    } else {
      xlow = x; xhigh = x;
    }
    if (y.getLevel() == minlevel) {
      ylow = y.low; yhigh = y.high;
    } else {
      ylow = y; yhigh = y;
    }
    if (z.getLevel() == minlevel) {
      zlow = z.low; zhigh = z.high;
    } else {
      zlow = z; zhigh = z;
    }

    result = makenode_internal(minvar,
                               ITE(xlow, ylow, zlow), 
                               ITE(xhigh, yhigh, zhigh));

    // put it in cache
    this.iteCache.put(x, y, z, result);
    return result;
  }

  //////////////////////////////////////////////
  // More complicated operations
  //////////////////////////////////////////////

  // replace a set of variables by constants
  protected JBddNode RESTRICT(JBddNode x, JBddNode var) {
    if (x.isConst() || var.isConst()) return x; 

    int xpos = x.getLevel();
    int vpos = var.getLevel();

    if (xpos == vpos) {
      // wow, the same variable
      // check it is position or negative form in var
      if (var.low == JBddConstNode.ZERO()) {
        // positive form
        return RESTRICT(x.high, var.high);
      } else if (var.high == JBddConstNode.ZERO()) {
        // negative form
        return RESTRICT(x.low, var.low);
      } else {
        throw new RuntimeException("the variable set of RESTRICT operator is invalid");
      }
    } else if (xpos < vpos) {
      // current variable is not in the set
      return makenode_internal(x.variable, 
                               RESTRICT(x.low, var), 
                               RESTRICT(x.high, var));
    } else {
      // a variable of the set is not show in the bdd tree
      if (var.low == JBddConstNode.ZERO()) {
        return RESTRICT(x, var.high);
      } else if (var.high == JBddConstNode.ZERO()) {
        return RESTRICT(x, var.low);
      } else {
        throw new RuntimeException("the variable set of RESTRICT operator is invalid");
      }
    }
  }

  // make a pair object of bdd variabls
  // replace a group of variables by another grounp of variables
  // node x points the root of a bdd tree,
  protected JBddNode REPLACE(JBddNode x, Map varmap) {
    JBddVarPairs pairs = new JBddVarPairs(varmap);
    return replace_internal(x, pairs);
  }

  private JBddNode replace_internal(JBddNode x, JBddVarPairs pairs) {
    if (x.isConst()) return x;
    if (pairs.stop(x)) return x;

    // recursively down to the bottom
    JBddNode xlow = replace_internal(x.low, pairs);
    JBddNode xhigh = replace_internal(x.high, pairs);
    
    // adjust orders
    JBddNode result = correctify(pairs.replacedBy(x.variable), xlow, xhigh);

    return result;
  }

  // correct the order before make a node
  private JBddNode correctify(JBddVariable var, JBddNode x, JBddNode y) {
    if (var.getLevel() < x.getLevel() && var.getLevel() < y.getLevel())
      return makenode_internal(var, x, y);

    // error case, if bdd contains variable to be replaced
    if (var.getLevel() == x.getLevel() || var.getLevel() == y.getLevel())
      throw new RuntimeException("REPLACE failed: bdd tree contains variables that are replacing targets");
    
    JBddNode result;
    // var in higher order than one of subtrees
    if (x.getLevel() == y.getLevel()) {
      JBddNode newx = correctify(var, x.low, y.low);
      JBddNode newy = correctify(var, x.high, y.high);
      result = makenode_internal(x.variable, newx, newy);
    } else if (x.getLevel() < y.getLevel()) {
      JBddNode newx = correctify(var, x.low, y);
      JBddNode newy = correctify(var, x.high, y);
      result = makenode_internal(x.variable, newx, newy);
    } else {
      JBddNode newx = correctify(var, x, y.low);
      JBddNode newy = correctify(var, x, y.high);
      result = makenode_internal(y.variable, newx, newy);
    }
    
    return result;
  }

  class JBddVarPairs {
    private JBddVariable[] mapping;
    private int lastpos;   // a shortcut to stop recursion
    JBddVarPairs(Map vpairs) {
      int numberOfVariables = bddVariables.length;
      this.mapping = new JBddVariable[numberOfVariables];
      System.arraycopy(bddVariables, 0, 
                       this.mapping, 0, 
                       numberOfVariables);
      this.lastpos = numberOfVariables - 1;
      Iterator mapset = vpairs.entrySet().iterator();
      while (mapset.hasNext()) {
        Map.Entry entry = (Map.Entry)mapset.next();
        JBddVariable srcvar = (JBddVariable)entry.getKey();
        JBddVariable dstvar = (JBddVariable)entry.getValue();
        
        int srcpos = srcvar.getLevel();
        this.mapping[srcpos] = dstvar;
        if (srcpos > this.lastpos) this.lastpos = srcpos; 
      }
    }

    // returns a variable replacing another variable
    JBddVariable replacedBy(JBddVariable var) {
      return this.mapping[var.getLevel()];
    }
    // should stop recursion?
    boolean stop(JBddNode node) {
      if (node.getLevel() > this.lastpos) 
        return true;
      else 
        return false;
    }
  }

  // replace a variable by a bdd, x[v/y]
  protected JBddNode COMPOSE(JBddNode x, JBddVariable v, JBddNode y) {
    throw new RuntimeException("not implemented yet");
  }

  // computer campact cofactors x | y
  //                              V
  protected JBddNode CONSTRAIN(JBddNode x, JBddNode y) {
    throw new RuntimeException("not implemented yet");
  }

  // simplify operator, f || g
  //                      \/
  // we use the same notion as BuDDy, the SIMPLIFY operator
  // is the restrict operator talked in Meinel and Theobald's book
  protected JBddNode SIMPLIFY(JBddNode x, JBddNode y) {
    throw new RuntimeException("not implemented yet");
  }

  ////////////////////////////////////////////////////
  // Quantifications
  ////////////////////////////////////////////////////
  // existential quantification  exits x.f
  // x is a set of variables to be quantified
  protected JBddNode EXISTENTIAL(JBddNode f, JBddNode x) {
    JBddVarSet vset = new JBddVarSet(x);
    return quantify_internal(f, vset, BDDOP_OR, x);
  }
  
  // universial quantification
  protected JBddNode UNIVERSAL(JBddNode f, JBddNode x) {
    JBddVarSet vset = new JBddVarSet(x);
    return quantify_internal(f, vset, BDDOP_AND, x);
  }

  // unique quantification
  protected JBddNode UNIQUE(JBddNode f, JBddNode x) {
    JBddVarSet vset = new JBddVarSet(x);
    return quantify_internal(f, vset, BDDOP_XOR, x);
  }

  // generalized quantification, op can be OR, AND, XOR
  private JBddNode quantify_internal(JBddNode f, JBddVarSet vars, int op,
                                     JBddNode x) {
    if (f.isConst()) return f;
    if (vars.stop(f)) return f;
   
    // look up cache first
    JBddNode result = this.quantCache.lookup(f, x, this.BDDOPERATORS[op]);
    if (result != null) return result;
    
    JBddNode flow  = quantify_internal(f.low, vars, op, x);
    JBddNode fhigh = quantify_internal(f.high, vars, op, x);
    
    if (vars.inSet(f.variable)) {
      result = apply_internal(flow, fhigh, op);
    } else {
      result = makenode_internal(f.variable, flow, fhigh);
    }

    this.quantCache.put(f, x, this.BDDOPERATORS[op], result);

    return result;
  }

  class JBddVarSet {
    private Set vars;
    private int lastpos = -1; // minimum order
    JBddVarSet(JBddNode v) {
      this.vars = new HashSet();
      // go on the positive edge 
      while (!v.isConst()) {
        this.vars.add(v.variable);
        int pos = v.variable.getLevel();
        if (pos > this.lastpos) this.lastpos = pos;

        v = v.high;
      }
    }

    boolean inSet(JBddVariable var) {
      return this.vars.contains(var);
    }
    
    boolean stop(JBddNode node) {
      return node.getLevel() > this.lastpos;
    }
  }

  //////////////////////////////////////////
  // Query, satisfication
  //////////////////////////////////////////
  
  //////////////////////////////////////////
  // Statistics, nodes number, cache hit rates, etc...
  //////////////////////////////////////////  
  /**
   * Reports the unique table and cache statistics.
   * @param out the print stream to print out statistics.
   */
  public void reportCacheStatistics(PrintStream out) {
    out.println("UniqueTable : ");
    this.uniqueTable.reportStatistics(System.out);
    out.println();
    out.println("ApplyCache :");
    this.applyCache.reportStatistics(System.out);
    out.println();
    out.println("IteCache :");
    this.iteCache.reportStatistics(System.out);
    out.println();
    out.println("quantCache :");
    this.quantCache.reportStatistics(System.out);
    out.println();
  }

  /**
   * Prints out configurations of unique table, and caches.
   */
  public void printConfigurations(PrintStream out) {
    out.print("Unique table : ");
    switch (this.UniqueTableKind) {
    case REGULAR_REF:
      out.println("regular "+this.UniqueTableSize);
      break;
    case SOFT_REF:
      out.println("soft "+this.UniqueTableSize);
      break;
    case WEAK_REF:
      out.println("weak "+this.UniqueTableSize);
      out.print("  Pooling ");
      switch (this.PoolingStrategy) {
      case NO_POOLING:
	out.print("none ");
	break;
      case PRE_ALLOCATION:
	out.print("pre-allocation ");
	break;
      case FIXED_SIZE:
	out.print("fixed ");
	break;
      case EXPANDIBLE:
	out.print("expandible ");
	break;
      case DYNAMIC:
	out.print("dynamic ");
	break;
      default:
	break;
      }
      out.println(this.NodePoolSize);
      break;
      default:
        break;
    }
    
    out.print("Cache kind ");
    switch (this.CacheKind) {
    case NO_CACHE:
      out.print("none, ");
      break;
    case REGULAR_REF:
      out.print("regular, ");
      break;
    case SOFT_REF:
      out.print("soft, ");
    }
    out.print("size "+this.CacheSize+", ");
    out.println("associativities "+this.CacheAssociativities);
  }
}
